package gov.nasa.jpf.symbc.modelcounter.sampler;

import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.lang.reflect.Modifier;
import java.net.URL;
import java.net.URLClassLoader;
import java.util.ArrayList;
import java.util.Stack;

import gov.nasa.jpf.jvm.ClassInfo;
import gov.nasa.jpf.symbc.numeric.BinaryLinearIntegerExpression;
import gov.nasa.jpf.symbc.numeric.BinaryNonLinearIntegerExpression;
import gov.nasa.jpf.symbc.numeric.BinaryRealExpression;
import gov.nasa.jpf.symbc.numeric.Constraint;
import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor;
import gov.nasa.jpf.symbc.numeric.Expression;
import gov.nasa.jpf.symbc.numeric.IntegerConstant;
import gov.nasa.jpf.symbc.numeric.IntegerExpression;
import gov.nasa.jpf.symbc.numeric.Operator;
import gov.nasa.jpf.symbc.numeric.RealConstant;
import gov.nasa.jpf.symbc.numeric.RealExpression;
import gov.nasa.jpf.symbc.numeric.SymbolicInteger;
import gov.nasa.jpf.symbc.numeric.SymbolicReal;
import gov.nasa.jpf.util.FileUtils;

/**
 * A visitor that evaluates constraints. Currently, the main use is the
 * different kinds of samplers.
 * 
 * @author Jaco Geldenhuys
 */
@SuppressWarnings("unused")
public class EvaluationVisitor extends ConstraintExpressionVisitor {

	public static enum Result {
		UNKNOWN, TRUE, FALSE, INVALID
	}

	/**
	 * The assignment (i.e., variable-value mapping) used during the evaluation.
	 */
	private Assignment assignment;

	/**
	 * Storage for intermediate values.
	 */
	private Stack<Object> stack;

	/**
	 * Indicates if something has gone wrong (such as division by zero, for
	 * instance).
	 */
	private boolean runtimeException;

	/**
	 * The final result. At the end of the visit, this should be either
	 * {@link Result#TRUE}, {@link Result#FALSE}, or {@link Result#INVALID} (if
	 * and only if {@link #runtimeException} is true). During the visit, the
	 * value is {@link Result#UNKNOWN}.
	 */
	private Result result;

	/**
	 * Prepare the visitor to perform an evaluation.
	 * 
	 * @param assignment
	 *            the variable value assignment to be used during the evaluation
	 */
	public EvaluationVisitor(Assignment assignment) {
		stack = new Stack<Object>();
		reset(assignment);
	}

	/**
	 * Reset the fields of the visitor to perform another evaluation.
	 * 
	 * @param assignment
	 *            the variable value assignment to be used during the evaluation
	 */
	public void reset(Assignment assignment) {
		this.assignment = assignment;
		stack.clear();
		runtimeException = false;
		result = Result.UNKNOWN;
	}

	/**
	 * Return the result of the evaluation.
	 * 
	 * @return the final result
	 */
	public Result getResult() {
		// assert expressionStack.isEmpty();
		return result;
	}

	/**
	 * Evaluate an integer expression given two integer values and an operator.
	 * 
	 * @param op
	 *            the operator
	 * @param l
	 *            the left-hand value
	 * @param r
	 *            the right-hand value
	 * @return the result of applying the operator to the given values
	 */
	private int evaluateIntegerOperation(Operator op, int l, int r) {
		switch (op) {
		case PLUS:
			return l + r;
		case MINUS:
			return l - r;
		case MUL:
			return l * r;
		case DIV:
			if (r == 0) {
				runtimeException = true;
				return 0;
			} else {
				return l / r;
			}
		case AND:
			return l & r;
		case OR:
			return l | r;
		case XOR:
			return l ^ r;
		case SHIFTL:
			return l << r;
		case SHIFTR:
			return l >> r;
		case SHIFTUR:
			return l >>> r;
		default:
			throw new RuntimeException("## Unknown operator " + op);
		}
	}

	/**
	 * Evaluate a real expression given two real values and an operator.
	 * 
	 * @param op
	 *            the operator
	 * @param l
	 *            the left-hand value
	 * @param r
	 *            the right-hand value
	 * @return the result of applying the operator to the given values
	 */
	private double evaluateRealOperation(Operator op, double l, double r) {
		switch (op) {
		case PLUS:
			return l + r;
		case MINUS:
			return l - r;
		case MUL:
			return l * r;
		case DIV:
			if (r == 0) {
				runtimeException = true;
				return 0.0;
			} else {
				return l / r;
			}
		default:
			throw new RuntimeException("## Unknown operator " + op);
		}
	}

	/**
	 * A placeholder routine that is (we hope) overloaded by a more specific
	 * routine for handling a specific kind of {@link Expression} subclass.
	 * 
	 * @param expr
	 *            the expression to "handle"
	 */
	@Override
	public void postVisit(Expression expr) {
		throw new RuntimeException("## Unknown expression " + expr);
	}

	/**
	 * Evaluate an integer, linear, binary expression by applying the operator
	 * to its left and right subexpressions. The subexpressions have already
	 * been visited and their values are waiting on the stack.
	 * 
	 * @param expr
	 *            the expression to evaluate
	 */
	@Override
	public void postVisit(BinaryLinearIntegerExpression expr) {
		int r = (Integer) stack.pop();
		int l = (Integer) stack.pop();
		stack.push(evaluateIntegerOperation(expr.getOp(), l, r));
	}

	/**
	 * Evaluate an integer, non-linear, binary expression. The action is
	 * identical to that of {@link #handle(BinaryLinearIntegerExpression)}.
	 * 
	 * @param expr
	 *            the expression to evaluate
	 */
	@Override
	public void postVisit(BinaryNonLinearIntegerExpression expr) {
		int r = (Integer) stack.pop();
		int l = (Integer) stack.pop();
		// Oh, the horror! Why is there no expr.getOp()?
		stack.push(evaluateIntegerOperation(expr.op, l, r));
	}

	/**
	 * Evaluate a real, binary expression by applying the operator to its left
	 * and right subexpressions. The subexpressions have already been visited
	 * and their values are waiting on the stack.
	 * 
	 * @param expr
	 *            the expression to evaluate
	 */
	@Override
	public void postVisit(BinaryRealExpression expr) {
		double r = (Double) stack.pop();
		double l = (Double) stack.pop();
		stack.push(evaluateRealOperation(expr.getOp(), l, r));
	}

	/**
	 * Evaluate an integer constant by placing its value on the stack.
	 * 
	 * @param expr
	 *            a description of the constant
	 */
	@Override
	public void postVisit(IntegerConstant expr) {
		stack.push(expr.value());
	}

	/**
	 * Evaluate a real constant by placing its value on the stack.
	 * 
	 * @param expr
	 *            a description of the constant
	 */
	@Override
	public void postVisit(RealConstant expr) {
		stack.push(expr.value());
	}

	/**
	 * Evaluate a symbolic integer by looking up its value in the visitor's
	 * variable value assignment.
	 * 
	 * @param expr
	 *            a description of the symbolic integer
	 */
	@Override
	public void postVisit(SymbolicInteger expr) {
		stack.push(assignment.getInt(expr.getName()));
	}

	/**
	 * Evaluate a symbolic real by looking up its value in the visitor's
	 * variable value assignment.
	 * 
	 * @param expr
	 *            a description of the symbolic real
	 */
	@Override
	public void postVisit(SymbolicReal expr) {
		stack.push(assignment.getDouble(expr.getName()));
	}

	/**
	 * Evaluate a constraint by applying the relational operators to the left
	 * and right expressions of the comparison. The expression have already been
	 * visited and their values are waiting on the stack. The
	 * {@link #runtimeException} signals that some kind of problem arose during
	 * the evaluation (such as division by zero). In this case the result is
	 * {@link Result#INVALID}. Otherwise, the result is either
	 * {@link Result#TRUE} or {@link Result#FALSE}, depending on the outcome of
	 * the comparison.
	 * 
	 * @param constraint
	 *            the constraint to evaluate
	 * @see gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor#postVisit(gov.nasa.jpf.symbc.numeric.Constraint)
	 */
	@Override
	public void postVisit(Constraint constraint) {
		if (runtimeException) {
			result = Result.INVALID;
		} else {
			double r = ((Number) stack.pop()).doubleValue();
			double l = ((Number) stack.pop()).doubleValue();
			result = constraint.getComparator().evaluate(l, r) ? Result.TRUE
					: Result.FALSE;
		}
	}

//	FOLLOWING CODE REMOVED FROM FunctionExpression.java
//	MAY BE NEEDED LATER ON...??
//	@Override
//	public Object evaluate(Assignment asgnmnt) {
//		assert (sym_args != null && sym_args.length > 0);
//		try {
//			if (clsLoader == null) {
//				ArrayList<String> list = new ArrayList<String>();
//				String[] cp = ClassInfo.getClassPathElements();
//				cp = FileUtils.expandWildcards(cp);
//				for (String e : cp) {
//					list.add(e);
//				}
//				URL[] urls = FileUtils.getURLs(list);
//				clsLoader = new URLClassLoader(urls);
//			}
//			Class<?> cls = null;
//			try {
//				cls = Class.forName(class_name, true, clsLoader);
//			} catch (ClassNotFoundException c) {
//				c.printStackTrace();
//				System.err.println("Class not found:" + class_name);
//			} catch (UnsatisfiedLinkError e) {
//				e.printStackTrace();
//				System.out.println("unsatisfied link error");
//			}
//			Object[] args = new Object[sym_args.length];
//			for (int i = 0; i < args.length; i++)
//				if (sym_args[i] instanceof IntegerExpression) {
//					args[i] = (Integer) ((IntegerExpression) sym_args[i]).evaluate(asgnmnt);
//				} else {// RealExpression
//					args[i] = (Double) ((RealExpression) sym_args[i]).evaluate(asgnmnt);
//				}
//			Method m = cls.getMethod(method_name, argTypes);
//			int modifiers = m.getModifiers();
//			if (Modifier.isStatic(modifiers) && Modifier.isPublic(modifiers)) {
//				Object result = null;
//				try {
//					result = m.invoke(null, args); // here we need the type of
//													// the result
//				} catch (InvocationTargetException e) {
//					e.printStackTrace();
//					System.err.println("exception :" + e.getMessage());
//				}
//				if (result instanceof Double) {
//					// System.out.println("result type is double");
//					return ((Double) result).doubleValue();
//				}
//				if (result instanceof Integer) {
//					// System.out.println("result type is int");
//					return ((Integer) result).doubleValue();
//				}
//				// System.out.println("result "+result);
//			}
//		}
//
//		catch (Throwable e) {
//			System.err.println(e);
//		}
//		return 0.0;
//	}

}
